\newpage
\section{Introduction}


J'ai effectué ce stage dans le cadre de ma troisième année de Licence en 
Informatique, sous la direction de Jean-Christophe Filliâtre (Equipe ProVal, 
LRI, Université Paris Sud 11 et CNRS / INRIA Saclay - Île-de-France). L'équipe 
ProVal a pour objectif de présenter des outils permettant de démontrer la 
validité de programmes par rapport à un comportement attendu en utilisant des
méthodes formelles de preuve.
Ces outils sont en majorité dévelopés en langage OCaml. 

Le but de mon stage n'est donc pas concentré sur le c\oe ur de métier de 
l'équipe. Il correspond plutôt à une contribution au langage OCaml. 
Cette contribution
prend la forme d'une bibliothèque pour la combinatoire, apportant
des méthodes simples permettant de modéliser des problèmes de combinatoire
sous forme de matrice de contraintes. Elle inclut l'implémentation de 
deux algorithmes permettant de résoudre le problème de la couverture exacte de
matrice ainsi qu'un langage pour décrire les problèmes de pavage.
